$\forall$${\it es}$:ES, ${\it ff}$:FIFO, $i$:${\it ff}$.C, $e$, ${\it e'}$:\{$e$:E$\mid$ ${\it ff}$.R($i$,$e$)\} , $j$:${\it ff}$.C.
\\[0ex](${\it ff}$.S($j$,$i$,${\it ff}$.Sender($i$,$e$)))
\\[0ex]$\Rightarrow$ (${\it ff}$.S($j$,$i$,${\it ff}$.Sender($i$,${\it e'}$)))
\\[0ex]$\Rightarrow$ (${\it ff}$.Sender($i$,$e$) = ${\it ff}$.Sender($i$,${\it e'}$) $\in$ E)
\\[0ex]$\Rightarrow$ ($e$ = ${\it e'}$)